sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
MAX(cons(u, l)) → MAX(l)
ST(n, l) → COND1(member(n, l), n, l)
GT(s(u), s(v)) → GT(u, v)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → MAX(l)
ST(n, l) → MEMBER(n, l)
COND1(false, n, l) → GT(n, max(l))
MEMBER(n, cons(m, l)) → MEMBER(n, l)
SORT(l) → ST(0, l)
EQUAL(s(x), s(y)) → EQUAL(x, y)
MAX(cons(u, l)) → IF(gt(u, max(l)), u, max(l))
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
MEMBER(n, cons(m, l)) → OR(equal(n, m), member(n, l))
MEMBER(n, cons(m, l)) → EQUAL(n, m)
MAX(cons(u, l)) → GT(u, max(l))
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MAX(cons(u, l)) → MAX(l)
ST(n, l) → COND1(member(n, l), n, l)
GT(s(u), s(v)) → GT(u, v)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → MAX(l)
ST(n, l) → MEMBER(n, l)
COND1(false, n, l) → GT(n, max(l))
MEMBER(n, cons(m, l)) → MEMBER(n, l)
SORT(l) → ST(0, l)
EQUAL(s(x), s(y)) → EQUAL(x, y)
MAX(cons(u, l)) → IF(gt(u, max(l)), u, max(l))
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
MEMBER(n, cons(m, l)) → OR(equal(n, m), member(n, l))
MEMBER(n, cons(m, l)) → EQUAL(n, m)
MAX(cons(u, l)) → GT(u, max(l))
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(u), s(v)) → GT(u, v)
The value of delta used in the strict ordering is 15/8.
POL(s(x1)) = 1/2 + (13/4)x_1
POL(GT(x1, x2)) = (15/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
MAX(cons(u, l)) → MAX(l)
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAX(cons(u, l)) → MAX(l)
The value of delta used in the strict ordering is 1/2.
POL(cons(x1, x2)) = 1/4 + (7/2)x_2
POL(MAX(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQUAL(s(x), s(y)) → EQUAL(x, y)
The value of delta used in the strict ordering is 15/8.
POL(EQUAL(x1, x2)) = (15/4)x_2
POL(s(x1)) = 1/2 + (13/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MEMBER(n, cons(m, l)) → MEMBER(n, l)
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MEMBER(n, cons(m, l)) → MEMBER(n, l)
The value of delta used in the strict ordering is 1/2.
POL(cons(x1, x2)) = 1/4 + (7/2)x_2
POL(MEMBER(x1, x2)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
ST(n, l) → COND1(member(n, l), n, l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v